COMMENT ⊗   VALID 00004 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	LET PASCAL(*,*,B,*) = {!PASCAL [INIT()] <BLOCK>!'.} MEAN
 00012 00003	EXPR GENCONDP(FLIST)
 00016 00004	EXPR FCN_ENTRYEXIT(L)
 00026 ENDMK
⊗;
LET PASCAL(*,*,B,*) = {!PASCAL [INIT()] <BLOCK>!'.} MEAN
	BEGIN
%B IS THE LIST <ENTRYCONDITION,EXITCONDITION,STATEMENT BODY>%
		TERPRI();
		PRINTSTR("PASCAL PROGRAM SUCCESSFULLY PARSED");
		GENCONDP(PROCEDURE_LIST);
		GENCONDM(B);
	END;
LET BLOCK(CR,PFD,*,CT) =
	{<CONDITION_RESULT>
	{REP 0 M *{{ALT <PROCEDURE_DECLARATION> |
	<DEFFUNDECL>|<VARIABLE_DECLARATION>}}}BEGIN <COMPOUND_TAIL>} MEAN
	BEGIN NEW X,Y;
	LOOP;	IF NULL PFD THEN RETURN CR@<CDR CT>;
		X←CAR PFD;
		PFD←CDR PFD;
		Y ← CDR X[1];
		IF X[1,1] = 1 THEN
			PROCEDURE_LIST←PROCEDURE_LIST@Y
		ELSE IF X[1,1]=2 THEN
			FUNCTION_LIST ← FUNCTION_LIST @ Y;
		GO LOOP
	END;
LET CONDITION_RESULT(PENTRY,*,EXIT,*) =
	{{OPT ENTRY <ASSERTION_EXPRESSION> '; } 
	EXIT <ASSERTION_EXPRESSION> '; }
	MEAN <IF PENTRY THEN PENTRY[2] ELSE 'TRUE, EXIT>;
LET PROCEDURE_DECLARATION(*,I,PL,*,B,*,*) =
	{PROCEDURE [IDENTIFIER] {OPT <PARAMETER_LIST>} '; 
	<PBLOCK> '; [FLUSH] } MEAN
	<I, PL,B>;
LET PBLOCK(CR,PFD,*,CT) =
	{<PCONDITION_RESULT>
	{REP 0 M *{{ALT <PROCEDURE_DECLARATION> |
	<DEFFUNDECL>|<VARIABLE_DECLARATION>}}}BEGIN <COMPOUND_TAIL>} MEAN
	BEGIN NEW X,Y;
	LOOP;	IF NULL PFD THEN RETURN CR@<CDR CT>;
		X←CAR PFD;
		PFD←CDR PFD;
		Y←CDR X[1];
		IF X[1,1]=1 THEN
			PROCEDURE_LIST←PROCEDURE_LIST@Y
		ELSE IF X[1,1]=2 THEN
			FUNCTION_LIST←FUNCTION_LIST@Y;
		GO LOOP
	END;
LET PCONDITION_RESULT(PENTRY,*,PEXIT,*)=
	{!ENTRY <INDEXED_ASSERT> '; 
	!EXIT <ASSERTION_EXPRESSION> '; }
	MEAN <PENTRY,PEXIT>;
LET DEFFUNDECL(*,I,PL,*,TY,*,CR,*)={DEFFUN [IDENTIFIER] <PARAMETER_LIST> 
	!': [IDENTIFIER] !'; <CONDITION_RESULT> [FLUSH]} MEAN<I,PL,CR,TY>;
LET VARIABLE_DECLARATION(*,TY) =
	{VAR{REP 1 M*{<IDENTIFIER_LIST> ': <PASCAL_TYPE> '; [FLUSH]
	}}} MEAN
	FOR NEW X IN TY DO
		IF CAR X[3,1] = 'ARRAY THEN
			FOR NEW Y IN X[1] DO
				ARRAY_LIST←(Y CONS CDR X[3])CONS ARRAY_LIST;
LET PARAMETER_LIST(*,S,*) = { '( 
	{REP 1 M *{{ALT<CONST_VAR_FCN_SPEC> |
	<PROCEDURE_SPEC>}}';} ') } MEAN
	BEGIN NEW SPEC, TYPE,J,X,Y,Z;
 	LOOP;	IF NULL S THEN RETURN J;
		X←CAR S;
		S←CDR S;
		SPEC ← X[1,2]; TYPE ← SPEC[3];
		Z←SPEC[2];
	LOOP1;	IF NULL Z THEN GO LOOP;
		Y←CAR Z;Z←CDR Z;
		J←J@<<Y,SPEC[1],TYPE>>;
		GO LOOP1
	END;
LET CONST_VAR_FCN_SPEC(S,IL,*,I) = {{OPT {ALT CONST | VAR | FUNCTION}}
	<IDENTIFIER_LIST> ': [IDENTIFIER]} MEAN
	IF NULL S THEN <'CONST, IL, I> ELSE <CADAR S, IL, I>;
LET PROCEDURE_SPEC(*,IL) = {PROCEDURE <IDENTIFIER_LIST>} MEAN
	<'PROCEDURE, IL, 'PROCEDURE>;
LET IDENTIFIER_LIST(I) = { {REP 1 M*{ [IDENTIFIER]}',}}
	MEAN I;
LET PASCAL_TYPE(KIND) = {{ALT ARRAY '[ <CONSTANT> '. '. <CONSTANT> '] OF
	[IDENTIFIER] | [IDENTIFIER]}} MEAN
	IF KIND[1] = 1 THEN <'ARRAY, KIND[4], KIND[7], KIND[10]>
	ELSE <'VARIABLE, KIND[2]>;
LET CONSTANT(KIND) = {{ALT [NUMBER] | [IDENTIFIER]}} MEAN CADR KIND;
LET COMPOUND_TAIL(S,*,*) = {
%Statements are orderd in reverse order%
	{REP 1 M *{{ALT [NUMBER]!': !<ASSERTION>|<STATEMENT>|<ASSERTION>}}';
	}!END  [FLUSH]} MEAN 
	BEGIN NEW J;
	FOR NEW X IN S DO
		IF X[1,1]=1 THEN LABEL_LIST←(X[1,2]CONS X[1,4,2])CONS LABEL_LIST
		ELSE IF X[1,2,1]='CMPD THEN J←CDR X[1,2]@J ELSE J←X[1,2]CONS J;
	J←'CMPD CONS J;
	RETURN J
	END;
LET STATEMENT(KIND) = {{OPT{ALT <ASSIGNMENT> | <COMPOUND> | <IF_STATEMENT> |
	<ASSERTION> | <WHILE_STATEMENT> | 
	<PROCEDURE_CALL> }}} MEAN IF KIND THEN CADAR KIND ELSE NIL;
LET ASSIGNMENT(V,*,E) = {<VARIABLE> {ALT '← | ': '=} <XPRESS>} MEAN 
	<'?←, V, E>;
LET COMPOUND(*,C) = {BEGIN <COMPOUND_TAIL>} MEAN C;
LET IF_STATEMENT(*,X1,*,S1,S2) = {IF <XPRESS> THEN <STATEMENT>
	{OPT ELSE <STATEMENT>}} MEAN 
	IF S2 THEN <'IFELSE, X1, S1, CADR S2>
	ELSE <'IF, X1, S1>;
LET INDEXED_ASSERT(ID,*,EX)={[IDENTIFIER] ': <ASSERTION_EXPRESSION>}
	MEAN	BEGIN NEW I;
		I←SHARPNAME(ID);
		RETURN I CONS SUBST(I,ID,EX)
		END;
LET ASSERTION(*,ASRT) = { ASSERT <ASSERTION_EXPRESSION> } MEAN
	<'ASRT, ASRT>;
LET WHILE_STATEMENT(*,X,*,EX,*,S) = {WHILE <XPRESS> '; <INDEXED_ASSERT> DO
	<STATEMENT>}
	MEAN <'WHILE, X, S,EX>;
LET PROCEDURE_CALL(I,*,XP,*) = { [IDENTIFIER] '( 
	{REP 1 M *{ <XPRESS> }',} ') } MEAN
	<'CALL,I,MAKECOMMAEXPR(FOR NEW X IN XP COLLECT X)>;
LET ASSERTION_EXPRESSION(AE1,AE) = { <XPRESS> {REP 0 M *{'& <XPRESS>}}}
	MEAN BEGIN NEW J;
	J ← AE1;
	FOR NEW X IN AE DO J ← <'?&, J, CADR X>;
	RETURN J;
	END;
LET XPRESS(RE,ORE) =
	{<RELATIONAL_EXPRESSION> {OPT {ALT '→ | '⊃} <RELATIONAL_EXPRESSION> }}
	MEAN IF ORE THEN <CADAR ORE, RE, CADR ORE> ELSE RE;
LET RELATIONAL_EXPRESSION(SE,OSE) = {<SIMPLE_EXPRESSION> {OPT 
	<RELATIONAL_OPERATOR> <SIMPLE_EXPRESSION>}} MEAN
	IF OSE THEN <CAR OSE, SE, CADR OSE> ELSE SE;
LET SIMPLE_EXPRESSION(A1,T1,TE) = { {OPT <ADDING_OPERATOR>} <TERM>
	{REP 0 M *{<ADDING_OPERATOR> <TERM>}}} MEAN
	BEGIN NEW J;
	IF A1 THEN J ← <CAR A1,T1> ELSE J ← T1;
	FOR NEW X IN TE DO J ← <CAR X, J, CADR X>;
	RETURN J;
	END;
LET TERM(F1,F) = {<FACTOR> {REP 0 M *{<MULT_OPERATOR> <FACTOR>}}} MEAN
	BEGIN NEW J;
	J ← F1;
	FOR NEW X IN F DO J ← <CAR X, J, CADR X>;
	RETURN J;
	END;
LET FACTOR(KIND) = {{ALT [IDENTIFIER] '( {REP 1 M*{<XPRESS>}',}')
	 | [NUMBER] | '( <XPRESS> ') |	'¬ <FACTOR> | <VARIABLE> |
	{ALT '∀ | '∃} {REP 1 M *{[IDENTIFIER]}',}
	'( <XPRESS> ') }}
	MEAN IF KIND[1] = 5 ∨ KIND[1] = 2 THEN KIND[2] ELSE
	IF KIND[1] = 3 THEN KIND[3] ELSE IF KIND[1] = 4 THEN
	<'?¬, KIND[3]> ELSE IF KIND[1] = 1 THEN
	<'FCN,KIND[2],MAKECOMMAEXPR(FOR NEW X IN KIND[4] COLLECT X)>
	ELSE
	BEGIN NEW J,K,L; K ← KIND[5];
	FOR NEW X IN KIND[3] DO BEGIN L←SHARPNAME(X[1]);J←IF J THEN<'?,,J,L>ELSE L;
	K←SUBST(L,X[1],K) END;RETURN <KIND[2,2], J, K>;
	END;
LET VARIABLE(I,SUB) = {[IDENTIFIER] {OPT '[ <XPRESS> '] }} MEAN
	IF SUB THEN <'ARRAY, I, SUB[2]> ELSE I;
LET RELATIONAL_OPERATOR(KIND) = {{ALT '= | '≠ | '< | '> | '≤ | '≥ }}
	MEAN CADR KIND;
LET ADDING_OPERATOR(KIND) = {{ALT '+ | '- | '∨}} MEAN CADR KIND;
LET MULT_OPERATOR(KIND) = {{ALT '* | '/ | '∧ | DIV | MOD}} MEAN
	CADR KIND;
%End of the Pascal syntax analyzer.%


EXPR GENCONDP(FLIST);
	PVCCOND←FOR NEW X IN FLIST COLLECT
		BEGIN NEW I;
			VCCOND←NIL;
			VCCOND←VCGEN(X[3,3],SUBST(<'?+,CAR X[3,1],1>,CAR X[3,1]
				,CDR X[3,1]),X[3,2])@VCCOND;
			VCCOND←VCGEN(OMEGASUBST(X[1],X[3,3]),SUBST(0,CAR X[3,1],CDR X[3,1]),
				X[3,2]);
			TERPRI();PRINT 'FOR;PRINC X[1];PRINT 'THE;PRINC LENGTH VCCOND;
			PRINTSTR(" THE VERIFICATION CONDITONS ARE:");
			I←1;
			IF NULL VCCOND THEN TERPRI() ALSO PRINT'VALID;
			<X[1]CONS(FOR NEW Y IN VCCOND COLLECT
				BEGIN   NEW RET;
					TERPRI();PRINT '?#;PRINC I;PRINC '? ;I←I+1;
					RET←APVC(Y);
					SHOW(12,RET);
					<RET>
				END)>
		END;

EXPR OMEGASUBST(I,A);
	IF ATOM A THEN A ELSE
	IF EQ(CAR A,'CALL)∧EQ(A[2],I) THEN '?π ELSE
	OMEGASUBST(I,CAR A)CONS OMEGASUBST(I,CDR A);

EXPR GENCONDM(B);
	BEGIN NEW I;
		VCCOND←NIL;
		VCCOND←VCGEN(B[3],B[1],B[2])@VCCOND;
		TERPRI();PRINTSTR("FOR THE MAIN PROGRAM");PRINC LENGTH VCCOND;
		PRINTSTR(" VERIFICATION CONDITIONS ARE:");
		I←1;
		IF NULL VCCOND THEN TERPRI() ALSO PRINT'VALID;
		MVCCOND←FOR NEW Y IN VCCOND COLLECT
			BEGIN   NEW RET;
				TERPRI();PRINT '?#;PRINC I;PRINC '? ;I←I+1;
				RET←APVC(Y);SHOW(12,RET);<RET>
			END
	END;
SPECIAL ASVAL,ARNAME,ARSUBS;
EXPR ARRAYSUBST(ASVAL,ARNAME,ARSUBS,S);
% ARNAME[ARSUBS]←ASVAL. Substitute for all occurrences of ARNAME in S. The 
newly created VC is returned as value.%
	IF NULL S THEN S ELSE
	IF ATOM S THEN S ELSE
	IF S[1]='ARRAY ∧S[2]=ARNAME THEN <'CONDEXP,<'?=,ARSUBS,S[3]>,ASVAL,
		<'ARRAY,S[2],ARRAYSUBST(ASVAL,ARNAME,ARSUBS,S[3])>> ELSE
	ARRAYSUBST(ASVAL,ARNAME,ARSUBS,S[1]) CONS ARRAYSUBST(ASVAL,ARNAME,
		ARSUBS,CDR S);


EXPR FCNLOCATE(XP, FCNNAMES);
%Append to the list FCNNAMES all function calls in the expression XP.
FCNNAMES contains elements in the form <function name, argument(s)>.%
	IF ATOM XP THEN FCNNAMES
	ELSE IF NULL CDDR XP THEN FCNNAMES @ FCNLOCATE(XP[2],NIL)
	ELSE IF XP[1] = 'FCN THEN FCNNAMES @ <CDR XP> @
		FCNLOCATE(XP[3], NIL)
	ELSE IF XP[1] = 'CONDEXP THEN FCNNAMES @ FCNLOCATE(XP[2], NIL)
		@ FCNLOCATE(XP[3], NIL) @ FCNLOCATE(XP[4], NIL)
	ELSE FCNNAMES @ FCNLOCATE(XP[2], NIL) @ FCNLOCATE(XP[3], NIL) ;

EXPR FCN_ENTRYEXIT(L);
%Given a list L in the form produced by FCNLOCATE, return <P, R> where 
P is the "anding" of the entry conditions (with actual parameters
substituted) for the functions in L, and where R is the "anding" of the
exit conditions.%
	BEGIN NEW FCN_INFO, QENTRY, PEXIT, POSITION, FORMAL,
	FCNNAME, FCNARGS,X;
	IF NULL L THEN RETURN NIL;
	X←CAR L;
	FCNNAME ← X[1]; FCNARGS ← DECOMMALIST(X[2]);
	FCN_INFO ← ASSOC(FCNNAME,FUNCTION_LIST);
	IF NULL FCN_INFO THEN PRINT FCNNAME
		ALSO PRINTSTR("NOT FOUND")
		ALSO QENTRY ← <'FCN, PRENAME(FCNNAME), X[2]>
		ALSO PEXIT ← <'FCN, RESNAME(FCNNAME), X[2]>
	ELSE BEGIN FCN_INFO←CDR FCN_INFO; QENTRY ← FCN_INFO[2,1];
		POSITION ← CONVCOMMA(FCN_INFO[1]);
		PEXIT ← ARGADD(FCNNAME,POSITION,FCN_INFO[2,2]);
		FORMAL←DECOMMALIST(POSITION);
		QENTRY←PARSUBST(FCNARGS,FORMAL,QENTRY);
		PEXIT←PARSUBST(FCNARGS,FORMAL,PEXIT);
		END;
	RETURN <QENTRY,PEXIT>CONS FCN_ENTRYEXIT(CDR L)
	END;

EXPR IDSUBST(EX,ID,VC);
	IF ATOM VC THEN(IF VC=ID THEN EX ELSE VC)ELSE
	IF CAR VC='FCN THEN<VC[1],VC[2],IDSUBST(EX,ID,VC[3])>ELSE
		CONS(IDSUBST(EX,ID,CAR VC),IDSUBST(EX,ID,CDR VC));

EXPR ARGADD(ID,PL,VC);
	IF ATOM VC THEN(IF VC=ID THEN<'FCN,ID,PL>ELSE VC)ELSE
	IF CAR VC='FCN THEN<VC[1],VC[2],ARGADD(ID,PL,VC[3])>ELSE
		CONS(ARGADD(ID,PL,CAR VC),ARGADD(ID,PL,CDR VC));

EXPR PARSUBST(ACTUAL,FORMAL,VC);
	IF ATOM VC THEN
		BEGIN
			NEW X,Y;
			X←ACTUAL;Y←FORMAL;
	   	A;	IF NULL X THEN RETURN VC ELSE
			IF NULL Y THEN TERPRI()
				ALSO RETURN NIL ELSE
			IF CAR Y=VC THEN RETURN CAR X ELSE
				Y←CDR Y ALSO X←CDR X
				ALSO GO A
		END ELSE
	IF LENGTH VC=2 THEN <VC[1],PARSUBST(ACTUAL,FORMAL,VC[2])>ELSE
	IF LENGTH VC=3 THEN <VC[1],PARSUBST(ACTUAL,FORMAL,VC[2]),PARSUBST
		(ACTUAL,FORMAL,VC[3])> ELSE <VC[1],PARSUBST(ACTUAL,FORMAL,
	VC[2]),PARSUBST(ACTUAL,FORMAL,VC[3]),PARSUBST(ACTUAL,FORMAL,VC[4])>;

EXPR DECOMMALIST(L);
%Given a comma-expression representing a list of expressions, produce
a list of the individual expressions.%
	IF ATOM L ∨ L[1] ≠ '?, THEN <L> ELSE
		DECOMMALIST(L[2]) @ <L[3]> ;

EXPR MAKECOMMAEXPR(L);
%Given a list of expresssions produce a single comma-expression of the
list elements.%
	BEGIN NEW ARGSEXPR;
	ARGSEXPR ← L[1];
	FOR NEW X IN CDR L DO ARGSEXPR ← <'?,, ARGSEXPR, X>;
	RETURN ARGSEXPR;
	END;

EXPR FCNCONDITIONS(E);
%If there are no function calls in E, then return NIL else return the
<P, R> from FCN_ENTRYEXIT.%
	FCN_ENTRYEXIT(FCNLOCATE(E,NIL));

EXPR SHARPNAME(ID);
%From the identifier ID produce the next name of the form ID#123.  The
suffixed integer is determined by the property list BOUND_VARIABLES.
The property is the identifier and the value on entry is the last used
counter value for that identifier.  Absence of the property means no
previous use; ID#0 becomes ID#  without the zero.%
	BEGIN NEW COUNTER,PAIR;
	PAIR ← ASSOC(ID,BOUND_VARIABLES);
	IF NULL PAIR THEN PAIR ← ID CONS 0 ALSO 
		BOUND_VARIABLES ← PAIR CONS BOUND_VARIABLES;
	RPLACD(PAIR,(CDR PAIR)+1);
	COUNTER ← INTERN MAKNAM (EXPLODE ID @ <'??, '?#> @
		EXPLODE CDR PAIR);
	RETURN COUNTER;
	END;

EXPR PRENAME(ID);
%From the identifier ID produce PRE_ID, i.e. same name with PRE_ prefixed.%
	INTERN MAKNAM(EXPLODE 'PRE @ <'??, '?_> @ EXPLODE ID);

EXPR RESNAME(ID);
%From the identifier ID produce RES_id, i.e. same name with RES_ prefixed.%
	INTERN MAKNAM(EXPLODE 'RES @ <'??, '?_> @ EXPLODE ID);

EXPR TABLE();
%Set up property list of hierarchies of the operators.%
	BEGIN
	PUTPROP('HIERARCHY,  9, '?&);
	PUTPROP('HIERARCHY, 10, '?→);
	PUTPROP('HIERARCHY, 10, '?⊃);
	PUTPROP('HIERARCHY,  9, '?,);
	FOR NEW X IN <'?=, '?≠, '?<, '?>, '?≤, '?≥> DO
		PUTPROP('HIERARCHY, 8, X);
	FOR NEW X IN <'?+, '?-, '?∨> DO
		PUTPROP('HIERARCHY, 6, X);
	FOR NEW X IN <'?*, '?/, '?∧, 'DIV, 'MOD> DO
		PUTPROP('HIERARCHY, 4, X);
	PUTPROP('HIERARCHY,  2, '?¬);
	END;

EXPR SHOW(PREC, FORMULA);
%Display expression FORMULA "after" an operator of precedence PREC.%
	IF ATOM FORMULA THEN PRINC FORMULA
	ELSE IF NULL CDDR FORMULA THEN
		PRINC FORMULA[1] ALSO SHOW(2,FORMULA[2])
	ELSE IF FORMULA[1] = 'FCN THEN
		PRINC FORMULA[2] ALSO PRINC '?(
		ALSO SHOW(12, FORMULA[3]) ALSO PRINC '?)
	ELSE IF FORMULA[1] = 'ARRAY THEN
		PRINC FORMULA[2] ALSO PRINC '?[
		ALSO SHOW(12, FORMULA[3]) ALSO PRINC '?]
	ELSE IF FORMULA[1] = 'CONDEXP THEN
		PRINC '?( ALSO PRINC '? IF?  ALSO SHOW(12, FORMULA[2])
		ALSO PRINC '? THEN?  ALSO SHOW(12, FORMULA[3])
		ALSO PRINC '? ELSE?  ALSO SHOW(12, FORMULA[4])
		ALSO PRINC '?)
	ELSE IF FORMULA[1] = '?∀ ∨ FORMULA[1] = '?∃ THEN
		PRINC FORMULA[1] ALSO SHOW(12, FORMULA[2])
		ALSO PRINC '?( ALSO SHOW(12, FORMULA[3])
		ALSO PRINC '?)
	ELSE BEGIN NEW HIER, OP, DIVMOD, LEFT;
		OP ← FORMULA[1]; DIVMOD ← OP = 'DIV ∨ OP = 'MOD;
		HIER ← GET('HIERARCHY, OP);
		LEFT ← (PREC LESSP HIER)∨OP='?→∨OP='?⊃∨OP='?-∨OP='?/∨DIVMOD;
		IF LEFT THEN PRINC '?(;
		SHOW(HIER,FORMULA[2]);
		IF DIVMOD THEN PRINC '?  ALSO PRINC OP ALSO PRINC '? 
			ELSE PRINC OP;
		SHOW(HIER,FORMULA[3]); 
		IF LEFT THEN PRINC '?);
	END;

FEXPR SAVEVC (FLIST);
	BEGIN
	NEW DEV;
	DEV ← 'DSK?:;
LOOP; 	IF NULL FLIST THEN RETURN 'FINISHED
	ELSE IF CAR LAST EXPLODE CAR FLIST EQ '?: 
		| ¬ATOM CAR FLIST & ¬ATOM CDAR FLIST
		THEN DEV ← CAR FLIST
		ALSO FLIST ← CDR FLIST
		ALSO GO LOOP;
	EVAL <'OUTPUT, 'DSK?:, (
		IF ATOM CAR FLIST THEN CAR FLIST
		ELSE FLIST[1,1]) CONS 'VC>;
	OUTC(T, NIL);
	EVAL <FUNCTION PARSE, DEV, CAR FLIST>;
	OUTC(NIL, T);
        PRINTSTR ("FILE CREATED: " CAT (IF ATOM CAR FLIST THEN CAR FLIST
		ELSE FLIST[1,1])CAT ".VC") ;
	FLIST ← CDR FLIST;
	GO LOOP;
	END;

LET PROGRAM(*) = {<PASCAL>} MEAN NIL;

_EOF_